Nuprl Lemma : reduce2_wf
4,23
postcript
pdf
A
,
T
:Type,
L
:
T
List,
k
:
A
,
i
:
,
f
:(
T
{
i
..(
i
+||
L
||)
}
A
A
). reduce2(
f
;
k
;
i
;
L
)
A
latex
Definitions
,
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
{
i
..
j
}
,
reduce2(
f
;
k
;
i
;
as
)
,
i
j
,
P
Q
,
False
,
A
,
A
B
,
P
&
Q
,
i
j
<
k
,
S
T
,
S
T
Lemmas
le
wf
,
non
neg
length
,
int
seg
wf
,
length
wf1
,
nat
wf
origin
A, T:Type, L:T List, k:A, i:
, f:(T
{i..(i+||L||)
}AA). reduce2(f;k;i;L) 
A A, T:Type, L:T List, k:A, i:, f:(T{i..(i+||L||)}AA). reduce2(f;k;i;L) A Tx:A. B(x)}
j
Q
A
B j < k
T
T